Inference at * 1 2 
Iof proof for Lemma member-exists:



1. T : Type
2. u : T
3. v : T List
4. x:T. (x  [u / v])
  ([u / v] = []) 

latex

 by ((D 0) 
CollapseTHEN (MaAuto)) 

latex

C1: 

C1: 5. [u / v] = []
C1:   False
C.

Definitions	A, P  Q, , False, (x  l), a < b, x:A. B(x), x:A  B(x), Type, , [car / cdr], x:A. B(x), x:AB(x), s = t, A List, t  T, [], type List
Lemmas	not wf, false wf